00100		COMMENT - Not all individuals are sets and ISSET X asserts
00200		that X is a set. ;
00300	GIVEAX(ISSET,(∀ X)(∀ Y)(XεY ⊃ ISSET Y));
00400	
00500	GIVEAX(EXTENSIONALITY,(∀ U)(∀ V)(ISSET U ∧ ISSET V ⊃
00600		((∀ X)(XεU ≡ XεV) ⊃ U=V)));
00700	
00800	GIVEAX(NULLSET,ISSET NULLSET);
00900	
01000	GIVEAX(NULL1,(∀ X)(¬(XεNULLSET)));
01100	
01200	GIVEAX(UNITSET,(∀ X)(∀ Y)(YεUNITSET(X)≡(Y=X)));
01300	
01400	GIVEAX(UNIONSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET (X ∪ Y)));
01500	
01600	GIVEAX(UNIONAX,(∀ X)(∀ Y)(∀ Z)(Zε(X ∪ Y)≡ZεX∨ZεY));
01700	
01800	GIVEAX(INTERSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET(X∩Y)));
01900	
02000	GIVEAX(INTER,(∀ X)(∀ Y)(∀ Z)(ZεX∩Y ≡ ZεX AND ZεY));
02100	
02200	GIVEAX(CARTSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET(X⊗Y)));
02300	
02400		COMMENT - We use the LISP . for the function that makes
02500		an ordered pair out of its members. ;
02600	GIVEAX(CARTESIAN,(∀ X)(∀ Y)(∀ Z)(Z ε X⊗Y ≡ 
02700		(∃ U)(∃ V)(UεX ∧ VεY ∧ Z=U.V)));
02800	
02900	GIVEAX(PAIR,(∀ X)(∀ Y)(∀ U)(∀ V)(X.Y=U.V ≡ X=U ∧ Y=V));
03000	
03100	GIVEAX(CONTAIN,(∀ U)(∀ V)(U⊂V ≡ (∀ X)(XεU ⊃ XεV)));
03200	
03300		COMMENT - The set of maps from X to Y. ;
03400	GIVEAX(POWERSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET(X→Y)
03500	∧(∀ F)(F ε (X→Y)⊃ISMAP F ∧ X=DOMAIN F ∧ Y = RANGE F)));
03600	
03700		COMMENT - We will make extensive use of the convention
03800		that each map has a domain and a range.  In particular,
03900		two maps are different if they have different ranges
04000		even if they have the same domains and take on the same
04100		values.  ;
04200	GIVEAX(MAP,(∀ F)(ISMAP F ⊃ ISSET DOMAIN F ∧ ISSET RANGE F
04300		Fε(DOMAIN F → RANGE F)));
04400	
04500	GIVEAX(APPLY,(∀ F)(∀ X)(∀ U)(∀ V)(Fε(U→V) ∧ XεU ⊃ β(F,X)εV));
04600	
04700	GIVEAX(FEXTENSIONALITY,(∀ U)(∀ V)(∀ F)(∀ G)(Fε(U→V) ∧ Gε(U→V) ⊃
04800		(F=G ≡ (∀ X)(XεU ⊃ β(F,X)=β(G,X)))));
04900	
05000	GIVEAX(FNDEF,(∀ FF)(∀ U)(∀ V)(ISSET U ∧ ISSET V ∧ ISSET FF ∧
05100		(FF ⊂ U⊗V) ∧ (∀ X)(XεU ⊃ (∃ Y)(YεV ∧ (X.Y)εFF)) ∧
05200		(∀ X)(∀ Y)(∀ Z)(XεU ∧ YεV ∧ X.Y ε FF ∧ X.Z ε FF ⊃ Y=Z)
05300					⊃
05400		(∃ F)(Fε(U→V)∧(∀ X)(XεU ⊃ X.β(F,X) ε FF))));
05500	
05600	GIVEAX(DIFFSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET(X-Y) ∧
05700		(∀ Z)(Zε(X-Y) ≡ ZεX ∧ ¬(ZεY))));
05800	
05900	GIVEAX(BIGUNION,(∀ X)(ISSET X ∧ (∀ Y)(YεX ⊃ ISSET Y) ⊃
06000		ISSET BIGUNION X ∧ (∀ Z)(ZεBIGUNION X ≡ (∃ Y)(
06100		YεX ∧ ZεY))));
06200	
06300	GIVEAX(BIGINTER,(∀ X)(ISSET X ∧ (∀ Y)(YεX ⊃ ISSET Y) ⊃
06400		ISSET BIGINTER X ∧ (∀ Z)(ZεBIGUNION X ≡ (∀ Y)(
06500		YεX ⊃ ZεY))));
06600	
06700	GIVESCHM(COMPREHENSION,(PRED PP)(∀ UU)(ISSET UU ⊃
06800		(∃ WW)(ISSET WW ∧ (∀ XX)(XXεWW ≡ XXεUU ∧ PP XX))));
06900	
07000	GIVEAX(RELATION,(∀ R)(RELATION R ≡ ISMAP R ∧
07100		RANGE R = (DOMAIN R → TV)));
07200	
07300	GIVEAX(TV,T≠ F ∧((∀ X)(XεTV ≡ X=T ∨ X=F)));
07400	
07500	GIVEAX(RRANGE,(∀ F)(ISMAP F ⊃ (∀ X)(XεRRANGE F ≡
07600		XεRANGE F ∧ (∃ Y)(YεDOMAIN F ∧ β(F,Y)=X))));
07700	
07800	GIVEAX(EASYREL,(∀ R)(RELATION R ⊃ (∀ X)(∀ Y)(β(β(R,X),Y)=T
07900	≡ββ(X,R,Y))));
08000	
08100	GIVEAX(BETA2,(∀ F)(∀ X)(∀ Y)(β2(F,X,Y)=β(β(F,X),Y)));
08200	
08300	GIVEAX(BETA3,(∀ F)(∀ X)(∀ Y)(∀ Z)(β3(F,X,Y,Z)=β(β(β(F,X),Y),Z)));
08400	
08500	GIVEAX(BETA4,(∀ F)(∀ X)(∀ Y)(∀ Z)(∀ W)(β4(F,X,Y,Z,W) =
08600		β(β(β(β(F,X),Y),Z),W)));
08700	
08800	GIVEAX(TRIVIAL,(∀ R)(∀ U)(TRIVIAL(R,U) ≡ RELATION R
08900		∧ ISSET U ∧ U ⊂ DOMAIN R ∧ (∀ X)(∀ Y)(XεU
09000			∧YεU ⊃ ββ(X,R,Y)=F)));
09100	
09200	GIVESCHM(FCOMPREHENSION,(PRED FF)(∀ U)(∀ V)(ISSET U ∧ ISSET V
09300	∧ (∀ X)(XεU ⊃ FF X ε V) ⊃ (∃ F)(Fε(U→V) ∧
09400	(∀ X)(XεU ⊃ β(F,X) = FF X))));
09500	
09600	GIVEAX(FINITE1,FINITE NULLSET);
09700	
09800	GIVEAX(FINITE2,(∀ U)(∀ X)(ISSET U ∧ FINITE U
09900		⊃ FINITE(U ∪ UNITSET X)));
10000	
10100	GIVEAX(INFINITE,(∀ U)(∀ V)(ISSET U ∧ ISSET V ∧ INFINITE U
10200		∧ FINITE V ⊃ (∃ X)(XεU ∧ ¬(XεV))));
     

00100	END;